R-state(R;i)
== case R of 
== Rnone => 
== Rplus(left,right)=>rec1,rec2.rec1  rec2
== Rinit(loc,T,x,v)=> if loc = i x : T else  fi
== Rframe(loc,T,x,L)=> if loc = i x : T else  fi
== Rsframe(lnk,tag,L)=> 
== Reffect(loc,ds,knd,T,x,f)=> if loc = i ds else  fi
== Rsends(ds,knd,T,l,dt,g)=> if source(l) = i ds else  fi
== Rpre(loc,ds,a,T,P)=> if loc = i ds else  fi
== Raframe(loc,k,L)=> 
== Rbframe(loc,k,L)=> 
== Rrframe(loc,x,L)=>  

latex

---

clarification:

R-state(R;i)
== case R of 
== Rnone => 
== Rplus(left,right)=>rec1,rec2.fpf-join(IdDeq;rec1;rec2)
== Rinit(loc,T,x,v)=> if loc = i x : T else  fi
== Rframe(loc,T,x,L)=> if loc = i x : T else  fi
== Rsframe(lnk,tag,L)=> 
== Reffect(loc,ds,knd,T,x,f)=> if loc = i ds else  fi
== Rsends(ds,knd,T,l,dt,g)=> if source(l) = i ds else  fi
== Rpre(loc,ds,a,T,P)=> if loc = i ds else  fi
== Raframe(loc,k,L)=> 
== Rbframe(loc,k,L)=> 
== Rrframe(loc,x,L)=>  

latex

Definitions	es realizer ind, f  g, IdDeq, x : v, source(l), if b t else f fi, a = b,
FDL editor aliases	R-state